package za.ac.sun.cs.distrib;

import za.ac.sun.cs.distrib.BounderService;
import za.ac.sun.cs.distrib.logging.LogWriter;
import za.ac.sun.cs.green.expr.IntVariable;
import gov.nasa.jpf.annotation.MJI;
import gov.nasa.jpf.symbc.numeric.SymbolicInteger;
import gov.nasa.jpf.vm.MJIEnv;
import gov.nasa.jpf.vm.NativePeer;

public class JPF_za_ac_sun_cs_distrib_Support extends NativePeer {

	@MJI
	public static int makeSymbolicInteger(MJIEnv env, int objRef, int stringRef) {
		String name = env.getStringObject(stringRef);
		SymbolicInteger x = new SymbolicInteger(name);
		BounderService.addVariable(new IntVariable(x.getName(), x, x._min, x._max));
		LogWriter.newvar(x.getName(), x._min, x._max);
		env.setReturnAttribute(x);
		return 0;
	}

}
